A, B, C:Type, g:(A(B + Top)), f:(ABC), x:A.
(can-apply(f o' g;x))  (do-apply(f o' g;x) ~ (f(x,do-apply(g;x)))) 

latex

ProofTree

Definitions	False, t  T, P  Q, b, True, left + right, Top, x:AB(x), x:A. B(x), s = t, f(a), do-apply(f;x), can-apply(f;x), f o' g, Type
Lemmas	true wf, false wf